\subsection{Representation of Types}\label{typeRep}
Types are built using one of 7 constructors. The exact definition for the representation scheme is:
\begin{samepage}
\begin{definition}[$<Type>$]
\begin{verbatim}

 <Type>   ::=   | TyVar <Int>
                | TyArr <Type> <Type>
                | TyAll <Type>
                | TyString
                | TyFloat
                | TyInt
                | TyUnit
\end{verbatim}
\end{definition}
\end{samepage} \noindent The last 4 constructors are the types that
we've described as being ``built in" the system. The first 3
constructors are used to build composite types. So that, for
example, the representation of the $\typ{TyBool}$ constant type,
when read in conjunction with context \ref{ListStr} is  $(TyVar\
9)$. However, when read with the same context, the type $\typ{\Pi X
. \AT{(\AT{X}{\AT{TyBool}{X}})}{X}}$  is represented by: {\small
\begin{verbatim}
TyAll(
  TyArr
    (TyArr (TyVar 0) (TyArr (TyVar 10) (TyVar 0)))
    (TyVar 0))
\end{verbatim}}
\noindent
Within the body of the $TyAll$ type constructor, the constant $(TyVar\ 0)$ represents the
closest bound variable of the expression and all the other elements of the context have had their index incremented by one. This is the reason
for which the representation of the $TyBool$ constant type is $(TyVar\ 10)$ inside the abstraction (as opposed to $(TyVar\ 9)$ outside of it). Compare with the representation of the type
\begin{equation}
\typ{\AT{TyBool}{(\Pi X . \AT{(\AT{X}{\AT{TyBool}{X}})}{X})}}
\end{equation}
which is represented within the ListStr context by the expression:
\begin{samepage}
{\small
\begin{verbatim}
TyArr
  (TyVar 9)
  (TyAll
    (TyArr
       (TyArr (TyVar 0) (TyArr (TyVar 10) (TyVar 0)))
       (TyVar 0)))
\end{verbatim}}
\end{samepage}
\noindent
The context of an expression may be the result of several shifts. For example, the type:
\begin{equation}
\typ{\Pi Y. \AT{Y}{\AT{(\Pi X. \AT{X}{Y})}{Y}}}
\end{equation}
\noindent
is represented as:
{\small
\begin{verbatim}
TyAll(
  TyArr
    (TyVar 0)
    (TyArr
        (TyAll (TyArr (TyVar 0) (TyVar 1)))
        (TyVar 0)))
\end{verbatim}}
\noindent
Here, the first bound variable ($Y$) appears as $(TyVar\ 1)$ in the innermost context, while
within the innermost context, $(TyVar\ 0)$ refers to the $X$ bound variable. Note that the representation for this term is invariant
under any context. This is because the type is a pure abstraction. Note also that it corresponds to the 2nd order logic  sentence:
\begin{equation}
\forall y. \AT{y}{\AT{(\forall x. \AT{x}{y})}{y}}
\end{equation}
in which all the variables are bound. This is not an accident. In fact, the representation of any expression that contains only bound variables is invariant with regard to the context in which it is read. Our representation scheme for types provides access to the efficient implementation of several predicated on types:
\begin{enumerate}
\item The $\mathit{typeSubstTop}$ operation, obtained directly from \cite{Pie02}, substitutes a type for a type variable bound
 within the abstract type.
\item The $\mathit{ty\_eqv}$ function takes two types as arguments and returns true when they are equivalent up to renaming/simplyfying constants. For example (when read with context \ref{ListStr}), both \ref{streq1} and \ref{steq2} evaluate to $true$.
    \begin{align}
    \label{streq1}
    \mathit{\mathit{ty\_eqv}}&\ [TyList]\ [\Pi X.\AT{X}{\AT{(\AT{String}{\AT{X}{X}})}{X}}]\\
    \label{steq2}
    \mathit{\mathit{ty\_eqv}}&\ [\Pi Y.\AT{Y}{\AT{(\AT{String}{\AT{Y}{Y}})}{Y}}]\ [\Pi X.\AT{X}{\AT{(\AT{String}{\AT{X}{X}})}{X}}]
    \end{align}



\item The $is\_constructor\_for$ function (pseudo-code: Program \ref{isConstructor}) indicates if objects of a given type can be used to construct objects of another type $B$ using only functional application. For example, both \ref{tiypPathEqun1} and \ref{tiypPathEqun2} below evaluate to true while \ref{tiypPathEqun3} evaluates to false.
\begin{align}\label{tiypPathEqun1}
\mathit{is\_constructor\_for}&\
    \typ{Int}\ \typ{\AT{Boolean}{\AT{Int}{Int}}}
    \\
\label{tiypPathEqun2}
\mathit{is\_constructor\_for}&\
    \typ{Boolean}\ \typ{(\Pi X.\AT{(\AT{Boolean}{X})}{\AT{\AT{X}{X})}{Boolean}}}\\
    \label{tiypPathEqun3}
\mathit{is\_constructor\_for}&\
    \typ{Int}\ \typ{\AT{Int}{\AT{Int}{Boolean}}}
\end{align}
\begin{Program}[h]
{\small
\begin{verbatim}
is_constructor_for constructed_ty function_ty =
    match function_ty with
     | _ when ty_eqv constructed_ty function_type --> true
     | TyArr _  tyRight --> is_constructor_for constructed_ty tyRight
     |_ --> false
\end{verbatim}}
\caption{The $is\_constructor\_for$ function}\label{isConstructor}
\end{Program}

\item The $\mathit{is\_data\_type}$ function (pseudo-code: Program \ref{isDataType}) indicates if a type is a data type as described in
section \ref{datatypeformat}.


\item The $type\_path$ function, (pseudo-code: Program \ref{typepathcode})
 indicates if a type $A$ is such that an object of type $A$ can be used as an application step to produce an object of type $C$. For example, both \ref{typPathEqun1} and \ref{typPathEqun2} below evaluate to true while \ref{typPathEqun3} evaluates to false.
\begin{align}\label{typPathEqun1}
\mathit{type\_path}&\
    \typ{\AT{Boolean}{\AT{Int}{Int}}}\
    \typ{Int}\\
\label{typPathEqun2}
\mathit{type\_path}&\
    \typ{\Pi X.\AT{(\AT{Boolean}{X})}{\AT{(\AT{X}{X})}{X}}}\
    \typ{Boolean}\\
    \label{typPathEqun3}
\mathit{type\_path}&\
    \typ{\AT{Int}{\AT{Int}{Boolean}}}\
    \typ{Int}
\end{align}
\begin{Program}[h]
{\small
\begin{verbatim}
type_path ty_beg ty_end =
   match (is_constructor_for ty_end ty_beg, is_data_type ty_beg) with
     | (true, _)   --> true
     | (_, true)   --> true
     | _           --> false
\end{verbatim}}
\caption{The $type\_path$ function}\label{typepathcode}
\end{Program}
\end{enumerate}

\begin{Program}[h]
{\small
\begin{verbatim}
is_data_type ty =

    let inner_ctx TyVar tyLeft tyRight =
    match (is_constructor_for tyVar tyLeft, tyRight) with
     |false, _ --> false
     |true, _ when ty_eqv tyVar tyRight --> true
     |true, (TyArr (tyLeft, tyRight))--> inner tyVar tyLeft tyRight
     |_->false in

     match ty with
    \end{verbatim}
    \begin{comment}
    The next subcase deals with the case where the variable
    is a name for a composed type
    \end{comment}
    \begin{verbatim}
      |TyVar index when is_name_for_composed_type index -->
        is_data_type (get_composed_type index)
    \end{verbatim}
    \begin{comment}
    if the type is an abstract type, then it might be
    the type of a data type
    \end{comment}
    \begin{verbatim}
    |TyAll (TyArr (tyLeft, tyRight)) -->
       let tyVar = the name of the bound
         type variable within the inner context of ty
       in inner_ctx tyVar tyLeft tyRight
    \end{verbatim}
    \begin{comment}
    if none of these two cases hold, then the type is not a data type
    \end{comment}
    \begin{verbatim}
    |_->false
\end{verbatim}}
\caption{The $\mathit{is\_data\_type}$ function}\label{isDataType}
\end{Program}


\subsection{Representation of Terms} Terms are represented using
one of 9 constructors. The exact definition is:
\begin{samepage}
\begin{definition}[$<Term>$]
\begin{verbatim}

 <Term>  ::= | TmVar <Int>
             | TmAbs <Type><Term>
             | TmApp <Term><Term>
             | TmTAbs <Term>
             | TmTApp <Term><Type>
             | TmString of  string
             | TmFloat <Float>
             | TmInt <Int>
             | TmUnit
\end{verbatim}
\end{definition}
\end{samepage}
\newpage
\noindent In which the $TmVar$ constructor points to an entry in the
term's associated context. Both the $TmAbs$ and the $TmTAbs$
constructors result in context shifting operations. For example, the
term \ref{hcjdhcd78}:
\begin{equation}\label{hcjdhcd78}
\Lambda X.\lambda x^{X}.\lambda y^{\AT{X}{X}}.y\ x
\end{equation}
is represented as:
\begin{verbatim}
TmTAbs(
  TmAbs (TyVar 0)
    (TmAbs (TyArr (TyVar 1) (TyVar 1))
      (TmApp (TmVar 0) (TmVar 1))))
\end{verbatim}
and is invariant with respect to the context in which it is read. This is not the case for the term \ref{xhbs673}:
\begin{equation}\label{xhbs673}
\lambda x^{TyInt}.plus\ x\ 4
\end{equation}
which, when read with context \ref{tab:ctxex1} (where $plus$ has index 1) is represented as:
\begin{verbatim}
(TmAbs TyInt
    (TmApp
        (TmApp (TmVar 2) (TmVar 0))
        (TmInt 4)))
\end{verbatim}
because the indexes of the names defined in the context are shifted by the number of binders in an expression, so the term $(TmVar\ 2)$, points to the name $plus$ of  context \ref{tab:ctxex1} as it is shifted by 1 binder because of the preceding $TmAbs$ constructor.
